perm filename MATCH.LSP[E84,JMC] blob
sn#758055 filedate 1984-07-08 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00009 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 declarations
C00005 00003 some basic axioms, not proved here.
C00006 00004 sort for match
C00007 00005 two simple facts about match
C00008 00006 the basic lemma
C00010 00007 the main lemma
C00017 00008 the final result
C00028 00009 (show)
C00049 ENDMK
C⊗;
; declarations
(wipe-out)
(get-proofs lispax prf prf jk)
(proof match)
(decl sublis (syntype: constant) (type:|ground⊗ground → ground|))
(decl match (syntype: constant) (type:|ground⊗ground⊗ground → ground|))
(decl isvar (syntype: constant) (type:|ground → truthval|) (unaryname: isvar))
(decl (p p1 p2) (type: ground) (sort: |sexp|))
(decl (e e1 e2) (type: ground) (sort: |sexp|))
(decl (b b1 b2) (type: ground) (sort: |alistp|))
(decl no (type: |ground|) (sort: |atom|) (syntype: constant))
(define sublis |∀ p p1 p2 b.
(atom p ⊃ sublis(p,b) = if isvar p then
if null assoc(p,b) then nil
else cdr assoc(p,b)
else p)
∧(sublis(p1.p2,b) = sublis(p1,b) . sublis(p2,b))|
(use sexpinductiondef))
(define matchfun |∀x y.
(atom x ⊃ matchfun(x) = λe b.
if isvar x then
if null assoc(x,b) then (x.e).b
else if cdr assoc(x,b) = e then b
else no
else if x = e then b else no)
∧(matchfun(x.y) = λe b.
if atom e then no
else if (matchfun(x))(car e,b) = no then no
else (matchfun (y))(cdr e,(matchfun (x))(car e,b)))|
(use high_order_definition
ue: ((bigfun . |λx y arb1 arb2. λe b.
if atom e then no
else if arb1(car e,b) = no then no
else arb2(cdr e, arb1(car e,b))|))))
(define match |∀p e b. match(p,e,b) = (matchfun(p))(e,b)|)
; some basic axioms, not proved here.
(label simpinfo mkalist assocdef alistdef)
(axiom |¬null no|)
(label simpinfo)
(axiom |∀x y. ¬null x.y|)
(label simpinfo)
(axiom |∀b. b ≠ no|)
(label simpinfo)
(axiom |∀x y. x.y ≠ no|)
(label simpinfo)
; sort for match
(der |∀p e b. atom p ⊃ (match(p,e,b)≠no ⊃ alistp match(p,e,b))|
()
(open match matchfun))
(ue (phi |λp.∀ e b. match(p,e,b)≠no ⊃ alistp match(p,e,b)|)
sexpinduction
(open matchfun match)
(use *))
(label simpinfo)
(label match_sort)
; two simple facts about match
; first, the pseudo-associativity
(trw |∀p1 p2 p3 e1 e2 e3.
(matchfun((p1.p2).p3))((e1.e2).e3,b) = (matchfun(p1.(p2.p3)))(e1.(e2.e3),b)|
(open matchfun))
(label associativity)
(trw |∀p1 p2 p3 e1 e2. ¬ atom e1 ⊃
(matchfun((p1.p2).p3))(e1.e2,b) =
(matchfun(p1.(p2.p3)))(car e1.(cdr e1.e2),b)|
(use cons_car_cdr mode: exact direction: reverse
associativity))
(label associativity_b)
;
(trw |∀p1 p2 e b.(matchfun(p1.p2))(e,b) ≠ no ⊃
(¬atom e ∧ (matchfun(p1))(car e,b) ≠ no)|
(part 1#1 (open matchfun)))
(label lemma_1)
; the basic lemma
; atomic case
(derive |∀xa ya e b. xa = ya ⊃
(((matchfun(xa))(e,b) ≠ no ∧ ¬null assoc(ya,b)) ⊃
assoc(ya,(matchfun(xa))(e,b)) = assoc(ya,b))|
()
(open matchfun))
(derive |∀xa ya e b. xa ≠ ya ⊃
(((matchfun(xa))(e,b) ≠ no ∧ ¬null assoc(ya,b)) ⊃
assoc(ya,(matchfun(xa))(e,b)) = assoc(ya,b))|
()
(open matchfun))
(derive |∀xa ya e b.((matchfun(xa))(e,b) ≠ no ∧ ¬null assoc(ya,b)) ⊃
assoc(ya,(matchfun(xa))(e,b)) = assoc(ya,b)|
(-1 -2))
; the induction step
(ue (phi |λp. ∀xa e b. match(p,e,b) ≠ no ∧ ¬null assoc(xa,b) ⊃
(assoc(xa,match(p,e,b)) = assoc(xa,b))|)
sexpinduction
(use *)
(open match))
(label l1)
(assume |match#l1#1#1#1#1|)
(label l2)
(assume |match#l1#1#1#1#2|)
(label l3)
(assume |match#l1#1#1#2#1#1|)
(label l4)
(rw *
(open matchfun))
(label l5)
(ue ((xa . |xa|) (e . |car e|) (b . |b|))
l2
(use l5))
(ue ((xa . |xa|) (e . |cdr e|) (b . |(matchfun(x))(car e,b)|))
l3
(use * l5))
(trw |match#l1#1#1#2#1#2|
(open matchfun)
(use * l5))
(ci (l4))
(ci (l2 l3))
(rw l1
(use *))
(label lemma_2)
; the main lemma
(ue (phi |λp1. ∀p2 e1 e2 b. match(p1.p2,e1.e2,b) ≠ no ⊃
e1 = sublis(p1,match(p1.p2,e1.e2,b))|)
sexpinduction
(open match))
(label l10)
(assume |match#l10#1#2#1#1#1|)
(label l11)
(assume |match#l10#1#2#1#1#2|)
(label l12)
(assume |match#l10#1#2#1#2#1#1|)
(label l13)
(ue ((p1 . |x.y|) (p2 . |p2|) (e . |e1.e2|) (b .|b|))
lemma_1
(use l13))
(label l14)
(ue ((p1 . |x|) (p2 . |y|) (e . |e1|) (b . |b|))
lemma_1
use * l13)
(label l14)
(rw l13
(use l14 associativity_b mode: exact))
(label l14)
(rw *
(use l14)
(nuse *)
(part 1#1#0 (open matchfun)))
(label l14)
(label simpinfo l13 l14)
(ue ((p2 . |y.p2|) (e1 . |car e1|) (e2 . |cdr e1.e2|) (b . |b|))
l11
(use associativity direction: reverse mode: exact))
(label l11a)
(ue ((p2 . |p2|) (e1 . |cdr e1|) (e2 . |e2|) (b . |(matchfun(x))(car e1,b)|))
l12)
(label l12a)
(trw |match#l10#1#2#1#2#1#2|
(open sublis))
(rw *
(part 2#2#2 (use associativity_b mode: exact)))
(rw *
(part 2#2#2#2#0 (open matchfun)))
(rw *
(use l11a mode: exact direction: reverse)
(use l12a mode: exact direction: reverse))
(unlabel simpinfo l13 l14)
(ci (l13))
(ci (l11 l12))
(rw l10
(use *))
(label l15)
(der |match#l15#1|
(lemma_2)
(part 1#2#1#1 (open matchfun))
(open sublis))
(rw l15
(use *))
(label lemma_3)
; the final result
(trw |∀p e b. atom p ⊃
((matchfun(p))(e,b)=no ∨ e = sublis(p,(matchfun(p))(e,b)))|
(open matchfun sublis))
(der |∀p. atom p ⊃
(∀e b. (matchfun(p))(e,b)≠no ⊃ e = sublis(p,(matchfun(p))(e,b)))|
*)
(label l21)
(ue (phi |λp.∀e b. match(p,e,b)≠no ⊃ e=sublis(p,match(p,e,b))|)
sexpinduction
(open match))
(rw *
(use l21))
(label l22)
(assume |match#l22#1#1#1|)
(label l23)
(assume |match#l22#1#1#2#1#1|)
(label l24)
(rw *
(open matchfun))
(label l25)
(trw |cdr e = sublis(y,(matchfun(y))(cdr e,(matchfun(x))(car e,b)))|
(use l23 l24 l25))
(label l26)
(trw |e = car e.cdr e|
(use l25)
(use cons_car_cdr direction: reverse))
(rw l24
(nuse cons_car_cdr)
(use * mode: exact))
(ue ((x . |x|) (p2 . |y|) (e1 . |car e|) (e2 . |cdr e|) (b . |b|))
lemma_3
(use l25 *))
(label l27)
(trw |match#l22#1#1#2#1#2|
(use l24)
(open sublis))
(rw *
(use l24 l25)
(part 2#2#1 (use l27 mode: exact direction: reverse))
(part 2#2#2#2#0 (open matchfun)))
(rw *
(use l25)
(part 2#2#2 (use l26 direction: reverse)))
(ci (l24))
(ci (l23))
(rw l22
(use *))
(label result)
(save-proofs match)
(show)
1. (DECL SUBLIS (SYNTYPE: CONSTANT) (TYPE: |(GROUND⊗GROUND)→GROUND|))
2. (DECL MATCH (SYNTYPE: CONSTANT) (TYPE: |(GROUND⊗GROUND⊗GROUND)→GROUND|))
3. (DECL ISVAR (SYNTYPE: CONSTANT) (TYPE: |GROUND→TRUTHVAL|)
(UNARYNAME: ISVAR))
4. (DECL (P P1 P2) (TYPE: |GROUND|) (SORT: |SEXP|))
5. (DECL (E E1 E2) (TYPE: |GROUND|) (SORT: |SEXP|))
6. (DECL (B B1 B2) (TYPE: |GROUND|) (SORT: |ALISTP|))
7. (DECL NO (TYPE: |GROUND|) (SORT: |ATOM|) (SYNTYPE: CONSTANT))
8. (DEFINE SUBLIS
|∀P P1 P2 B.(ATOM P⊃
SUBLIS(P,B)=
(IF ISVAR P
THEN (IF NULL ASSOC(P,B) THEN NIL ELSE CDR ASSOC(P,B))
ELSE P))∧SUBLIS(P1.P2,B)=SUBLIS(P1,B).SUBLIS(P2,B)|
(USE SEXPINDUCTIONDEF))
9. (DEFINE MATCHFUN
|∀X Y.(ATOM X⊃
MATCHFUN(X)=
(λE B.(IF ISVAR X
THEN (IF NULL ASSOC(X,B) THEN (X.E).B
ELSE (IF CDR ASSOC(X,B)=E THEN B ELSE NO))
ELSE (IF X=E THEN B ELSE NO))))∧
MATCHFUN(X.Y)=
(λE B.(IF ATOM E THEN NO
ELSE (IF (MATCHFUN(X))(CAR E,B)=NO THEN NO
ELSE (MATCHFUN(Y))
(CDR E,(MATCHFUN(X))(CAR E,B)))))|
(USE HIGH_ORDER_DEFINITION UE:
((BIGFUN.|λX Y ARB1 ARB2.(λE B.(IF ATOM E THEN NO
ELSE (IF ARB1(CAR E,B)=NO THEN
NO
ELSE ARB2(CDR E,
ARB1(CAR E,
B)))))|))))
10. (DEFINE MATCH |∀P E B.MATCH(P,E,B)=(MATCHFUN(P))(E,B)| NIL)
;labels: SIMPINFO
11. (AXIOM |¬NULL NO|)
;labels: SIMPINFO
12. (AXIOM |∀X Y.¬NULL X.Y|)
;labels: SIMPINFO
13. (AXIOM |∀B.¬B=NO|)
;labels: SIMPINFO
14. (AXIOM |∀X Y.¬X.Y=NO|)
15. (DERIVE |∀P E B.ATOM P⊃(¬MATCH(P,E,B)=NO⊃ALISTP MATCH(P,E,B))| ()
(OPEN MATCH MATCHFUN))
;labels: SIMPINFO MATCH_SORT
16. (UE ((PHI.|λP.(∀E B.¬MATCH(P,E,B)=NO⊃ALISTP MATCH(P,E,B))|)) SEXPINDUCTION
((OPEN MATCHFUN MATCH) (USE 15)))
;∀X E B.¬(MATCHFUN(X))(E,B)=NO⊃ALISTP (MATCHFUN(X))(E,B)
;labels: ASSOCIATIVITY
17. (TRW
|∀P1 P2 P3 E1 E2 E3.(MATCHFUN((P1.P2).P3))((E1.E2).E3,B)=
(MATCHFUN(P1.(P2.P3)))(E1.(E2.E3),B)|
(OPEN MATCHFUN))
;∀P1 P2 P3 E1 E2 E3.(MATCHFUN((P1.P2).P3))((E1.E2).E3,B)=
; (MATCHFUN(P1.(P2.P3)))(E1.(E2.E3),B)
;labels: ASSOCIATIVITY_B
18. (TRW
|∀P1 P2 P3 E1 E2.¬ATOM E1⊃
(MATCHFUN((P1.P2).P3))(E1.E2,B)=
(MATCHFUN(P1.(P2.P3)))(CAR E1.(CDR E1.E2),B)|
(USE CONS_CAR_CDR MODE: EXACT DIRECTION: REVERSE ASSOCIATIVITY))
;∀P1 P2 P3 E1 E2.¬ATOM E1⊃
; (MATCHFUN((P1.P2).P3))(E1.E2,B)=
; (MATCHFUN(P1.(P2.P3)))(CAR E1.(CDR E1.E2),B)
;labels: LEMMA_1
19. (TRW
|∀P1 P2 E B.¬(MATCHFUN(P1.P2))(E,B)=NO⊃
¬ATOM E∧¬(MATCHFUN(P1))(CAR E,B)=NO|
(PART 1#1 (OPEN MATCHFUN)))
;∀P1 P2 E B.¬(MATCHFUN(P1.P2))(E,B)=NO⊃¬ATOM E∧¬(MATCHFUN(P1))(CAR E,B)=NO
20. (DERIVE
|∀XA YA E B.XA=YA⊃
(¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃
ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B))| ()
(OPEN MATCHFUN))
21. (DERIVE
|∀XA YA E B.¬XA=YA⊃
(¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃
ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B))| ()
(OPEN MATCHFUN))
22. (DERIVE
|∀XA YA E B.¬(MATCHFUN(XA))(E,B)=NO∧¬NULL ASSOC(YA,B)⊃
ASSOC(YA,(MATCHFUN(XA))(E,B))=ASSOC(YA,B)| (21 20) NIL)
;labels: L1
23. (UE
((PHI.|λP.(∀XA E B.¬MATCH(P,E,B)=NO∧¬NULL ASSOC(XA,B)⊃
ASSOC(XA,MATCH(P,E,B))=ASSOC(XA,B))|)) SEXPINDUCTION
((USE 22) (OPEN MATCH)))
;(∀X Y.(∀XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
; ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B))∧
; (∀XA E B.¬(MATCHFUN(Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
; ASSOC(XA,(MATCHFUN(Y))(E,B))=ASSOC(XA,B))⊃
; (∀XA E B.¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
; ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B)))⊃
;(∀X XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
; ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B))
;labels: L2
24. (ASSUME
|∀XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B)|)
;deps: (L2)
;labels: L3
25. (ASSUME
|∀XA E B.¬(MATCHFUN(Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
ASSOC(XA,(MATCHFUN(Y))(E,B))=ASSOC(XA,B)|)
;deps: (L3)
;labels: L4
26. (ASSUME |¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)|)
;deps: (L4)
;labels: L5
27. (RW L4 (OPEN MATCHFUN))
;¬(ATOM E∨(MATCHFUN(X))(CAR E,B)=NO∨
; (MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B))=NO)∧¬NULL ASSOC(XA,B)
;deps: (L4)
28. (UE ((XA.|XA|) (E.|CAR E|) (B.|B|)) L2 (USE L5))
;ASSOC(XA,(MATCHFUN(X))(CAR E,B))=ASSOC(XA,B)
;deps: (L2 L4)
29. (UE ((XA.|XA|) (E.|CDR E|) (B.|(MATCHFUN(X))(CAR E,B)|)) L3 (USE 28
L5))
;ASSOC(XA,(MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))=ASSOC(XA,B)
;deps: (L2 L3 L4)
30. (TRW |ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B)|
((OPEN MATCHFUN) (USE 29 L5)))
;ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B)
;deps: (L2 L3 L4)
31. (CI (L4) 30 NIL)
;¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
;ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B)
;deps: (L2 L3)
32. (CI (L2 L3) 31 NIL)
;(∀XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
; ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B))∧
;(∀XA E B.¬(MATCHFUN(Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
; ASSOC(XA,(MATCHFUN(Y))(E,B))=ASSOC(XA,B))⊃
;(¬(MATCHFUN(X.Y))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
; ASSOC(XA,(MATCHFUN(X.Y))(E,B))=ASSOC(XA,B))
;labels: LEMMA_2
33. (RW L1 (USE 32))
;∀X XA E B.¬(MATCHFUN(X))(E,B)=NO∧¬NULL ASSOC(XA,B)⊃
; ASSOC(XA,(MATCHFUN(X))(E,B))=ASSOC(XA,B)
;labels: L10
34. (UE
((PHI.|λP1.(∀P2 E1 E2 B.¬MATCH(P1.P2,E1.E2,B)=NO⊃
E1=SUBLIS(P1,MATCH(P1.P2,E1.E2,B)))|))
SEXPINDUCTION (OPEN MATCH))
;(∀X.ATOM X⊃
; (∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))))∧
;(∀X Y.(∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))∧
; (∀P2 E1 E2 B.¬(MATCHFUN(Y.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(Y,(MATCHFUN(Y.P2))(E1.E2,B)))⊃
; (∀P2 E1 E2 B.¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))))⊃
;(∀X P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))
;labels: L11
35. (ASSUME
|∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))|)
;deps: (L11)
;labels: L12
36. (ASSUME
|∀P2 E1 E2 B.¬(MATCHFUN(Y.P2))(E1.E2,B)=NO⊃
E1=SUBLIS(Y,(MATCHFUN(Y.P2))(E1.E2,B))|)
;deps: (L12)
;labels: L13
37. (ASSUME |¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO|)
;deps: (L13)
;labels: L14
38. (UE ((P1.|X.Y|) (P2.|P2|) (E.|E1.E2|) (B.|B|)) LEMMA_1 (USE L13))
;¬(MATCHFUN(X.Y))(E1,B)=NO
;deps: (L13)
;labels: L14
39. (UE ((P1.|X|) (P2.|Y|) (E.|E1|) (B.|B|)) LEMMA_1 (USE L14 L13))
;¬ATOM E1∧¬(MATCHFUN(X))(CAR E1,B)=NO
;deps: (L13)
;labels: L14
40. (RW L13 (USE L14 ASSOCIATIVITY_B MODE: EXACT))
;¬(MATCHFUN(X.(Y.P2)))(CAR E1.(CDR E1.E2),B)=NO
;deps: (L13)
;labels: L14
41. (RW 40 ((USE L14) (NUSE 40) (PART 1#1#0 (OPEN MATCHFUN))))
;¬(MATCHFUN(Y.P2))(CDR E1.E2,(MATCHFUN(X))(CAR E1,B))=NO
;deps: (L13)
;labels: L11A
42. (UE ((P2.|Y.P2|) (E1.|CAR E1|) (E2.|CDR E1.E2|) (B.|B|)) L11
(USE ASSOCIATIVITY DIRECTION: REVERSE MODE: EXACT))
;CAR E1=SUBLIS(X,(MATCHFUN((X.Y).P2))(E1.E2,B))
;deps: (L11 L13)
;labels: L12A
43. (UE ((P2.|P2|) (E1.|CDR E1|) (E2.|E2|) (B.|(MATCHFUN(X))(CAR E1,B)|))
L12
NIL)
;CDR E1=SUBLIS(Y,(MATCHFUN(Y.P2))(CDR E1.E2,(MATCHFUN(X))(CAR E1,B)))
;deps: (L12 L13)
44. (TRW |E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))| (OPEN SUBLIS))
;E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))≡
;E1=
;SUBLIS(X,(MATCHFUN((X.Y).P2))(E1.E2,B)).
;SUBLIS(Y,(MATCHFUN((X.Y).P2))(E1.E2,B))
;deps: (L13)
45. (RW 44 (PART 2#2#2 (USE ASSOCIATIVITY_B MODE: EXACT)))
;E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))≡
;E1=
;SUBLIS(X,(MATCHFUN((X.Y).P2))(E1.E2,B)).
;SUBLIS(Y,(MATCHFUN(X.(Y.P2)))(CAR E1.(CDR E1.E2),B))
;deps: (L13)
46. (RW 45 (PART 2#2#2#2#0 (OPEN MATCHFUN)))
;E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))≡
;E1=
;SUBLIS(X,(MATCHFUN((X.Y).P2))(E1.E2,B)).
;SUBLIS(Y,(MATCHFUN(Y.P2))(CDR E1.E2,(MATCHFUN(X))(CAR E1,B)))
;deps: (L13)
47. (RW 46
((USE L11A MODE: EXACT DIRECTION: REVERSE)
(USE L12A MODE: EXACT DIRECTION: REVERSE)))
;E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))
;deps: (L11 L12 L13)
48. (CI (L13) 47 NIL)
;¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO⊃E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B))
;deps: (L11 L12)
49. (CI (L11 L12) 48 NIL)
;(∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))∧
;(∀P2 E1 E2 B.¬(MATCHFUN(Y.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(Y,(MATCHFUN(Y.P2))(E1.E2,B)))⊃
;(¬(MATCHFUN((X.Y).P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X.Y,(MATCHFUN((X.Y).P2))(E1.E2,B)))
;labels: L15
50. (RW L10 (USE 49))
;(∀X.ATOM X⊃
; (∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))))⊃
;(∀X P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))
51. (DERIVE
|∀X.ATOM X⊃
(∀P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B)))| (LEMMA_2)
((PART 1#2#1#1 (OPEN MATCHFUN)) (OPEN SUBLIS)))
;labels: LEMMA_3
52. (RW L15 (USE 51))
;∀X P2 E1 E2 B.¬(MATCHFUN(X.P2))(E1.E2,B)=NO⊃
; E1=SUBLIS(X,(MATCHFUN(X.P2))(E1.E2,B))
53. (TRW |∀P E B.ATOM P⊃(MATCHFUN(P))(E,B)=NO∨E=SUBLIS(P,(MATCHFUN(P))(E,B))|
(OPEN MATCHFUN SUBLIS))
;∀P E B.ATOM P⊃(MATCHFUN(P))(E,B)=NO∨E=SUBLIS(P,(MATCHFUN(P))(E,B))
;labels: L21
54. (DERIVE
|∀P.ATOM P⊃(∀E B.¬(MATCHFUN(P))(E,B)=NO⊃E=SUBLIS(P,(MATCHFUN(P))(E,B)))|
(53) NIL)
55. (UE ((PHI.|λP.(∀E B.¬MATCH(P,E,B)=NO⊃E=SUBLIS(P,MATCH(P,E,B)))|))
SEXPINDUCTION (OPEN MATCH))
;(∀X.ATOM X⊃(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B))))∧
;(∀X Y.(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧
; (∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))⊃
; (∀E B.¬(MATCHFUN(X.Y))(E,B)=NO⊃E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))))⊃
;(∀X E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))
;labels: L22
56. (RW 55 (USE L21))
;(∀X Y.(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧
; (∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))⊃
; (∀E B.¬(MATCHFUN(X.Y))(E,B)=NO⊃E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))))⊃
;(∀X E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))
;labels: L23
57. (ASSUME
|(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧
(∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))|)
;deps: (L23)
;labels: L24
58. (ASSUME |¬(MATCHFUN(X.Y))(E,B)=NO|)
;deps: (L24)
;labels: L25
59. (RW L24 (OPEN MATCHFUN))
;¬(ATOM E∨(MATCHFUN(X))(CAR E,B)=NO∨
; (MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B))=NO)
;deps: (L24)
;labels: L26
60. (TRW |CDR E=SUBLIS(Y,(MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))|
(USE L23 L24 L25))
;CDR E=SUBLIS(Y,(MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))
;deps: (L23 L24)
61. (TRW |E=CAR E.CDR E| ((USE L25) (USE CONS_CAR_CDR DIRECTION: REVERSE)))
;E=CAR E.CDR E
;deps: (L24)
62. (RW L24 ((NUSE CONS_CAR_CDR) (USE 61 MODE: EXACT)))
;¬(MATCHFUN(X.Y))(CAR E.CDR E,B)=NO
;deps: (L24)
;labels: L27
63. (UE ((X.|X|) (P2.|Y|) (E1.|CAR E|) (E2.|CDR E|) (B.|B|)) LEMMA_3
(USE L25 62))
;CAR E=SUBLIS(X,(MATCHFUN(X.Y))(E,B))
;deps: (L24)
64. (TRW |E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))| ((USE L24) (OPEN SUBLIS)))
;E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))≡
;E=SUBLIS(X,(MATCHFUN(X.Y))(E,B)).SUBLIS(Y,(MATCHFUN(X.Y))(E,B))
;deps: (L24)
65. (RW 64
((USE L24 L25) (PART 2#2#1 (USE L27 MODE: EXACT DIRECTION: REVERSE))
(PART 2#2#2#2#0 (OPEN MATCHFUN))))
;E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))≡
;E=CAR E.SUBLIS(Y,(MATCHFUN(Y))(CDR E,(MATCHFUN(X))(CAR E,B)))
;deps: (L24)
66. (RW 65 ((USE L25) (PART 2#2#2 (USE L26 DIRECTION: REVERSE))))
;E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))
;deps: (L23 L24)
67. (CI (L24) 66 NIL)
;¬(MATCHFUN(X.Y))(E,B)=NO⊃E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B))
;deps: (L23)
68. (CI (L23) 67 NIL)
;(∀E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B)))∧
;(∀E B.¬(MATCHFUN(Y))(E,B)=NO⊃E=SUBLIS(Y,(MATCHFUN(Y))(E,B)))⊃
;(¬(MATCHFUN(X.Y))(E,B)=NO⊃E=SUBLIS(X.Y,(MATCHFUN(X.Y))(E,B)))
;labels: RESULT
69. (RW L22 (USE 68))
;∀X E B.¬(MATCHFUN(X))(E,B)=NO⊃E=SUBLIS(X,(MATCHFUN(X))(E,B))
70.